Example 3.2 in [Lucas - PLILP'97]

Summary: Ex3_2_Luc97

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (Extra variables)

  CS-TRS Ex3_2_Luc97 (file Ex3_2_Luc97.csr)

  Functions:  dbl 0 s dbls nil cons sel indx from
  
  Constructors:  0 s nil cons
  
  Variables:  X Y Z
  
  Arities: 
  
  ar(dbl) = 1
  ar(0) = 0
  ar(s) = 1
  ar(dbls) = 1
  ar(nil) = 0
  ar(cons) = 2
  ar(sel) = 2
  ar(indx) = 2
  ar(from) = 1
  
  Replacement map: 
  
  µ(dbl)={1}
  µ(0)={}
  µ(s)={1}
  µ(dbls)={1}
  µ(nil)={}
  µ(cons)={}
  µ(sel)={1,2}
  µ(indx)={1}
  µ(from)={}
  
  Rules:  (file Ex3_2_Luc97) 
  
  dbl(0) -> 0
  dbl(s(X)) -> s(s(dbl(X)))
  dbls(nil) -> nil
  dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y))
  sel(0,cons(X,Y)) -> X
  sel(s(X),cons(Y,Z)) -> sel(X,Z)
  indx(nil,X) -> nil
  indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z))
  from(X) -> cons(X,from(s(X)))
  

  The CS-TRS in OBJ format (file Ex3_2_Luc97.obj):

  obj Ex3_2_Luc97 is
    sort S .
    op dbl : S -> S .
    op 0 : -> S .
    op s : S -> S .
    op dbls : S -> S .
    op nil : -> S .
    op cons : S S -> S [strat (0)] .
    op sel : S S -> S .
    op indx : S S -> S [strat (1 0)] .
    op from : S -> S [strat (0)] .
    vars X Y Z : S .
    eq dbl(0) = 0 .
    eq dbl(s(X)) = s(s(dbl(X))) .
    eq dbls(nil) = nil .
    eq dbls(cons(X,Y)) = cons(dbl(X),dbls(Y)) .
    eq sel(0,cons(X,Y)) = X .
    eq sel(s(X),cons(Y,Z)) = sel(X,Z) .
    eq indx(nil,X) = nil .
    eq indx(cons(X,Y),Z) = cons(sel(X,Z),indx(Y,Z)) .
    eq from(X) = cons(X,from(s(X))) .
  endo
  

  Negative results

  1. The µ-termination of Ex3_2_Luc97 cannot be proved by using Lucas' transformation. The TRS Ex3_2_Luc97_L:

         dbl(0) -> 0
         dbl(s) -> s
         dbls(nil) -> nil
         dbls(cons) -> cons
         sel(0,cons) -> X
         sel(s,cons) -> sel(X,Z)
         indx(nil) -> nil
         indx(cons) -> cons
         from -> cons
         

     contains extra variables.